%
% A BUNCH OF COMMANDS PUT IN BY DARPAN FOR THE DYNAMIC SEMANTICS
%
%
\urlstyle{rm}
\lstset{basicstyle=\codesize\ttfamily, numbers=left, numberstyle=\tiny, language=java,moredelim=[il][\codesize\sffamily]{?}, mathescape=true,showspaces=false,showstringspaces=false,columns=fullflexible,frame=single,}

\def\assign{\mathrel{\mathop:}=}

\newcommand{\vb}{\ensuremath{~\big{|}~}}

\newcommand{\inferlbl}[3] {\inferrule{#3}{#2}{\textsf{\footnotesize{\sc #1}}}}

\newcommand{\lambdaE}[3]{\ensuremath{\lambda #1 \ #2 {\Rightarrow} \ #3}}
\newcommand{\newE}[1] {\ensuremath{\textsf{new}} \ #1}
\newcommand{\caseE}[3] {\ensuremath{#1 : #2 \ \Rightarrow \ #3}}
\newcommand{\withE}[2] {\ensuremath{#1\  \textsf{with} \ #2}}
\newcommand{\plusEqE}[2] {\ensuremath{#1 \ += #2}}
\newcommand{\minusEqE}[2] {\ensuremath{#1 \ -= #2}}
\newcommand{\matchE}[2]{\ensuremath{\textsf{match} \ #1 \ \{#2\}}}

% 
% END NEW COMMANDS FOR DYNAMIC SEMANTICS
%
%

\section{Semantics}

\TODO{Please note: this section is currently out of date with respect to the
rest of the document}

\subsection{Expressions}

\[
\begin{array}{c}
\begin{array}{rrrll}
 & p & ::= & x~~|~~l\\
\emph{Values} & v & ::= & \fn\ x [r] => e~~|~~l \\
\emph{Expressions} & e & ::= & x~~|~~l~~\fn\ x [r] => e
                   ~~|~~e\ e~~|~~e.f~~|~~e.f = e\\
                   &   & |   & e <- \nterm{path} \{ \nterm{decls} \}
                   ~~|~~\match\ e \{ \nterm{cases} \}\\
                   &   & |   & \keyw{new}\ \nterm{implstate}\ 
                                           \nterm{comprises}_\emph{opt}\\
 & \nterm{case} & ::= & \nterm{path} => e \\
 & r            & ::= & \keyw{true}~~|~~r*r~~|~~r|r~~|~~r\&r~~|~~p:\tau\\
 & \nterm{path} & ::= & p~~|~~\nterm{path}.f~~|~~\nterm{path}\ \nterm{path}\\
 & \nterm{comprises}_\emph{opt} & ::= &\bullet~~|~~\nterm{comprises}\ 
                                                   \nterm{path}\\
 & \nterm{paths} & ::= & \bullet~~|~~\nterm{paths}, \nterm{path}\\
 & \nterm{implstate} & ::= & \nterm{path}
                   ~~|~~\nterm{implstate}\ \with\ \nterm{implstate}
                   ~~|~~\{ \nterm{decls} \} \\
 & \mu & ::= & \bullet
               ~~|~~\mu, l ->\ \extend\ l\ \extend\ \with\ \nterm{decls}\\
 & \Sigma & ::= & \bullet~~|~~\Sigma, l:\extend\ l\ \with\ \nterm{decls}\\
 & \Gamma & ::= & \bullet~~|~~\Gamma, x:\nterm{state}
\end{array}
\end{array}
\]

%\begin{verbatim}
%
%p ::= x
%  |   l
%
%v ::= fn x [r] => e
%  |   l
%
%e ::= x
%  |   l
%  |   fn x [r] => e
%  |   e e
%  |   e.f
%  |   e.f = e                     // could be subsumed by e <- ...
%  |   e <- path { decls }
%  |   match e { cases }           // could use case function instead
%  |   new implstate comprises_opt // could use case function for comprises
%
%case ::= path => e
%
%r ::= true
%  |   r * r
%  |   r | r
%  |   r & r
%  |   p:tau
%
%path ::= p
%     |   path . f
%     |   path path // only for constant functions
%
%comprises_opt ::= * | comprises paths
%
%paths ::= * | paths, path
%
%implstate ::= path
%          |   implstate with implstate
%          |   { decls }
%
%mu ::= * | mu, l -> extend l with decls
%
%sigma ::= * | sigma, l : extend l with decls
%
%gamma ::= * | gamma, x : state // simplify: path or extend path with typedecls?
%
%\end{verbatim}

\subsection{Declarations}

\[
\begin{array}{c}
\begin{array}{rrrll}
 & \nterm{decl} & ::= & \keyw{mutable}_\emph{opt} f:\tau = e_\emph{opt}
   ~~|~~\keyw{conserved}_\emph{opt}\ \keyw{type}\ t:\nterm{kind}\\
 & \nterm{kind} & ::= & \keyw{Type}~~|~~\keyw{State}~~|~~S(\tau)
                        ~~|~~S(\nterm{state})~~|~~\keyw{Subtype}(\tau)
                        ~~|~~\keyw{Subtype}(\nterm{state})\\
\end{array}
\end{array}
\]

%\begin{verbatim}
%
%decl ::= mutable_opt f:tau = e_opt // if missing then required
%     |   conserved_opt type t : kind
%
%kind ::= Type
%     |   State
%     |   S(tau)
%     |   Subtype(tau)
%     |   S(state)
%     |   Subtype(state)
%
%\end{verbatim}

\subsection{Types}
\[
\begin{array}{c}
\begin{array}{rrrll}
 \emph{Types} & \tau & ::= & \nterm{perm}\ \nterm{state} @ \nterm{state}
              ~~|~~\Pi x[r]\ \keyw{const}_\emph{opt}\ \Sigma y[r]
              ~~|~~\nterm{path}~~|~~\tau \& \tau\\
 & \nterm{state} & ::= & \nterm{path}
                 ~~|~~\nterm{state}\ \keyw{as}\ t\ \with\ \nterm{state}
                 ~~|~~\{ \nterm{typedecls} \} \\
 & \nterm{perm}  & ::= & \keyw{unique}~~|~~\keyw{shared}
                 ~~|~~\keyw{immutable}~~|~~\keyw{none}\\
 & \nterm{typedecls} & ::= & \bullet~~|~~\nterm{typedecls}\ \nterm{typedecl}\\
 & \nterm{typedecl}  & ::= & \keyw{mutable}_\emph{opt}\ 
                     \keyw{require}_\emph{opt}\ f:\tau\ 
                     \keyw{conserved}_\emph{opt}\ 
                     \keyw{require}_\emph{opt}\ 
                     \keyw{type}\ t:\nterm{kind}\\
\end{array}
\end{array}
\]


%\begin{verbatim}
%
%
%tau ::= perm state @ state
%    |   Pi x [r] . const_opt Sigma y [r]
%    |   path
%    |   tau & tau // intersection types for functions
%
%state ::= path
%      |   state as t with state  // do we need "as t"?
%      |   { typedecls }
%
%perm ::= unique
%     |   shared
%     |   immutable
%     |   none
%
%typedecls ::= * | typedecls typedecl
%
%typedecl ::= mutable_opt require_opt f:tau
%         |   conserved_opt require_opt type t : kind
%
%\end{verbatim}

\openi{Do we need fractions?  At least ``half''?}

\openi{How is borrowing done?  do we need a borrowed keyword, or
captured?  Assuming output fraction is the same as input is
problematic if you have two inputs to the same object and only one
output.}

\openi{Subtyping with parameters.  Since Plaid has structural subtyping,
perhaps we should handle covariance/contravariance automatically (and
structurally)}

\openi{Specifications.  In addition to typestates, it would be nice to
associate pre/post conditions - and maybe external invariants - with
interfaces and functions in interfaces.  We should also allow unit tests
for interfaces, which must be fulfilled by any implementation}


\subsection{Compilation}

\[
  \begin{array}{|c|}
  \hline
  \emph{Expr} ==> e \\
  \hline
  \end{array}
\]

\begin{mathpar}
  \inferrule{}
    {\keyw{fn}\ (\nterm{args})[\nterm{args}]\ \keyw{=>}\ \nterm{Expr} ==>}

  \and

  \inferrule{}
    {\keyw{let}\ x = \nterm{Expr}_1\ \keyw{in}\ \nterm{Expr}_2 ==>}

  \and

  \inferrule{}
    {\nterm{Expr}.f ==> }

  \and

  \inferrule{}
    {\nterm{Expr}_1 = \nterm{Expr}_2 ==>}

  \and

  \inferrule{}
    {\keyw{match}\ \nterm{Expr} \{ \nterm{CaseClauses} \} ==>}

  \and

  \inferrule{}
    {\nterm{Expr}\ \keyw{<-}\ [\nterm{QualifiedIdentifier}] 
     \{ \nterm{Decls} \} ==>}

  \and

  \inferrule{}
    {\nterm{Expr}_1 \nterm{Expr}_2 ==>}

  \and

  \inferrule{}
    {\keyw{new}\ \nterm{QualifierIdentifier} \{ \nterm{Decls} \} ==>}
\end{mathpar}

\[
  \begin{array}{|c|}
  \hline
  \nterm{Decl} ==> \nterm{Decl}\\
  \hline
  \end{array}
\]

\[
  \begin{array}{|c|}
  \hline
  \nterm{CompilationUnit} ==> e\\
  \hline
  \end{array}
\]

%\begin{verbatim}
%
%
%judgment rewrite-expr: Expr ==> e
%
%
%------------------------------------------
%fn (args) [args] => Expr ==> 
%
%
%------------------------------------------
%let x = Expr1 in Expr2 ==>
%
%
%------------------------------------------
%Expr.f ==> 
%
%
%------------------------------------------
%Expr1.f = Expr2 ==> 
%
%
%------------------------------------------
%match Expr1 { CaseClauses } ==> 
%
%
%------------------------------------------
%Expr1 <- [QualifiedIdentifier] { decls } ==> 
%
%------------------------------------------
%Expr1 Expr2 ==> 
%
%
%------------------------------------------
%new QualifiedIdentifier { decls } ==> 
%
%
%
%
%judgment rewrite-decl: decl ==> decl
%
%judgment rewrite-package: CompilationUnit ==> e
%
%
%\end{verbatim}

\subsection{Dynamic Semantics}

This section describes the dynamic semantics of Plaid. The language syntax is described in Figure \ref{fig:syntax}, and the dynamic semantics in Figure \ref{fig:dyn-sem}.

\begin{figure*}
%\fbox{
%\begin{minipage}{\myColumnWidth}
\[
\begin{array}{r c c l}
    \mbox{(Expressions)} & e & ::= &
        \lambdaE{x}{}{e} \\
    & & &
       e \ e \\
    & & &
        e.f \\ 
    & & &
        \plusEqE{e}{is} \vb \minusEqE{e}{is} \\
    & & &
    	\newE{is} \\
    & & &
    	\matchE{e}{\overline{case}} \\
    & & &
    	x \vb l \\
    \mbox{(Values)} & v & ::= &
    	\lambdaE{x}{}{e} \\
        & & &
        l \\
    \mbox{(Cases)} & case & ::= &
    	\caseE{x}{path}{e} \\
    \mbox{(Paths)} & path & ::= &
    	p \vb path.f \vb path \ path \\
    \mbox{} & p & ::= &
    	x \vb v \\
    \mbox{(Impl States)} & is & ::= &
    	path \\
    & & & 
	f = e \\
    & & &
	\withE{is}{is} \\
    \mbox{(Impl Sigs)} & ig & ::= &
    	path \\
    & & &
	f \\
    & & &
	\withE{ig}{ig} \\
    \mbox{(Stores)} & \mu & ::= &
    	\mu, l \mapsto os \vb
	\emptyset \\
    \mbox{(Obj States)} & os & ::= &
        f=v \vb \\
    & & &
        l \\
    & & &
        \withE{os}{os}\\
\end{array}
\]
%\end{minipage} 
%} %fbox end
\caption{Syntax}
\label{fig:syntax}
\end{figure*}

\begin{figure*}
%\fbox{
%\begin{minipage}{\pagewidth}
\fbox{$e \vb \mu \longmapsto e \vb \mu$}
\begin{mathpar}
\inferlbl{E-Apply}
	{(\lambdaE{x}{}{e}) v \vb \mu \longmapsto [v/x]e \vb \mu}
	{ }
\and
\inferlbl{E-Apply-Left}
	{e_1 \ e_2 \vb \mu \longmapsto e_1' \ e_2 \vb \mu'}
	{e_1 \vb \mu \longmapsto e_1' \vb \mu'}
\and
\inferlbl{E-Apply-Right}
	{v \ e \vb \mu \longmapsto v \ e' \vb \mu'}
	{e \vb \mu \longmapsto e' \vb \mu' }
\and
\inferlbl{E-New-Cong}
	{\newE{is} \vb \mu \longmapsto \newE{is'} \vb \mu'}
	{is \vb \mu \longmapsto is' \vb \mu' }
\and
\inferlbl{E-New}
	{\newE{os} \vb \mu \longmapsto l \vb [l \mapsto os] \mu}
	{l \notin \mu }
\and
\inferlbl{E-Decl-Cong}
	{f=e \vb \mu \longmapsto f=e' \vb \mu'}
	{e \vb \mu \longmapsto e' \vb \mu' }
\and
\inferlbl{E-Field}
	{l.f \vb \mu \longmapsto v \vb \mu}
	{\mu[l] = os \\ \mu \vdash os[f] = v}
\and
\inferlbl{E-PlusEquals}
	{\plusEqE{l}{os} \vb \mu \longmapsto l \vb [l \mapsto \withE{os'}{os}] \mu}
	{\mu[l] = os'}
\and
\inferlbl{E-MinusEqualsIg}
	{\minusEqE{l}{\withE{ig_1}{ig_2}} \vb \mu \longmapsto \minusEqE{l}{ig_2} \vb \mu'}
	{\minusEqE{l}{ig_1} \vb \mu \longmapsto l \vb \mu'}
\and
\inferlbl{E-MinusEqualsLoc}
	{\minusEqE{l}{l'} \vb \mu \longmapsto l \vb [l \mapsto os'] \mu}
	{\mu[l] = os \\ os' = os - l'}
\and
\inferlbl{E-MinusEqualsField}
	{\minusEqE{l}{f} \vb \mu \longmapsto l \vb [l \mapsto os'] \mu}
	{\mu[l] = os \\ os' = os - f}
\and
\inferlbl{E-Match-1}
	{\matchE{l}{\caseE{x}{l'}{e}, \overline{case}} \vb \mu \longmapsto [l/v]e \vb \mu}
	{\mu[l] = os \\ os <: l'}
\and
\inferlbl{E-Match-2}
	{\matchE{l}{\caseE{x}{l'}{e}, \overline{case}} \vb \mu \longmapsto \matchE{l}{\overline{case}} \vb \mu}
	{\mu[l] = os \\ os \nless: l'}
\end{mathpar}
%\end{minipage}

\caption{Dynamic semantics}
\label{fig:dyn-sem}
\end{figure*}

\begin{figure*}
%\fbox{
%\begin{minipage}{\pagewidth}
\fbox{$\mu \vdash os[f] = v$}
\begin{mathpar}
\inferlbl{Field}
	{\mu \vdash (f=v)[f] = v}
	{ }
\and
\inferlbl{Loc}
	{\mu \vdash l[f] = v}
	{\mu[l] = os \\ \mu \vdash os[f]=v}
\and
\inferlbl{With-1}
	{\mu \vdash (\withE{os_1}{os_2})[f] = v}
	{\mu \vdash os_2[f]=v}
\and
\inferlbl{With-2}
	{\mu \vdash (\withE{os_1}{os_2})[f] = v}
	{\mu \nvdash os_2[f]=v' \\ \mu \vdash os_1[f] = v}
\and

\end{mathpar}
%\end{minipage}
%} fbox end
\caption{Auxiliary judgments for dynamic semantics}
\label{fig:aux-dyn-sem}
\end{figure*}


\begin{figure}
  \includegraphics{PLTRedex/plaid-core-v1/plaid-core-syntax}
\end{figure}

\begin{figure}
  \includegraphics{PLTRedex/plaid-core-v1/plaid-core-reductions}
\end{figure}

\begin{figure}
  \includegraphics{PLTRedex/plaid-core-v1/plaid-core-helpers}
\end{figure}

\subsection{Properties}

Type soundness

Pure object-oriented model (as in Cook's Onward! '09 essay)

